D(t) → 1
D(constant) → 0
D(+(x, y)) → +(D(x), D(y))
D(*(x, y)) → +(*(y, D(x)), *(x, D(y)))
D(-(x, y)) → -(D(x), D(y))
↳ QTRS
↳ DependencyPairsProof
D(t) → 1
D(constant) → 0
D(+(x, y)) → +(D(x), D(y))
D(*(x, y)) → +(*(y, D(x)), *(x, D(y)))
D(-(x, y)) → -(D(x), D(y))
D1(+(x, y)) → D1(y)
D1(*(x, y)) → D1(y)
D1(-(x, y)) → D1(x)
D1(-(x, y)) → D1(y)
D1(+(x, y)) → D1(x)
D1(*(x, y)) → D1(x)
D(t) → 1
D(constant) → 0
D(+(x, y)) → +(D(x), D(y))
D(*(x, y)) → +(*(y, D(x)), *(x, D(y)))
D(-(x, y)) → -(D(x), D(y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
D1(+(x, y)) → D1(y)
D1(*(x, y)) → D1(y)
D1(-(x, y)) → D1(x)
D1(-(x, y)) → D1(y)
D1(+(x, y)) → D1(x)
D1(*(x, y)) → D1(x)
D(t) → 1
D(constant) → 0
D(+(x, y)) → +(D(x), D(y))
D(*(x, y)) → +(*(y, D(x)), *(x, D(y)))
D(-(x, y)) → -(D(x), D(y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D1(+(x, y)) → D1(y)
D1(-(x, y)) → D1(x)
D1(-(x, y)) → D1(y)
D1(+(x, y)) → D1(x)
Used ordering: Polynomial interpretation [25,35]:
D1(*(x, y)) → D1(y)
D1(*(x, y)) → D1(x)
The value of delta used in the strict ordering is 1/2.
POL(-(x1, x2)) = 1/2 + (4)x_1 + x_2
POL(*(x1, x2)) = (5/2)x_1 + (5/4)x_2
POL(D1(x1)) = (2)x_1
POL(+(x1, x2)) = 1/4 + (5/2)x_1 + (7/2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
D1(*(x, y)) → D1(y)
D1(*(x, y)) → D1(x)
D(t) → 1
D(constant) → 0
D(+(x, y)) → +(D(x), D(y))
D(*(x, y)) → +(*(y, D(x)), *(x, D(y)))
D(-(x, y)) → -(D(x), D(y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
D1(*(x, y)) → D1(y)
D1(*(x, y)) → D1(x)
The value of delta used in the strict ordering is 1/2.
POL(*(x1, x2)) = 1/4 + (5/2)x_1 + (5/2)x_2
POL(D1(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
D(t) → 1
D(constant) → 0
D(+(x, y)) → +(D(x), D(y))
D(*(x, y)) → +(*(y, D(x)), *(x, D(y)))
D(-(x, y)) → -(D(x), D(y))